﻿using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using TSU.FAMC.ComputerEngineering.Classes.Bdds.Basis;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Functions;
using TSU.FAMC.ComputerEngineering.Classes.Enums;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Fundamental;

namespace TSU.FAMC.ComputerEngineering.Classes.Bdds
{
    /// <summary>
    /// Represents an abstract binary-descision-diagram, a base class for Bdds
    /// </summary>
    public class BaseBdd
    {
        /// <summary>
        /// Top-level nodes.
        /// </summary>
        public List<Node> Roots = new List<Node>();

        /// <summary>
        /// Terminal nodes.
        /// </summary>
        public List<Node> Sinks = new List<Node>();

        /// <summary>
        /// Counts number of nodes in bdd by rounding graph for each root.
        /// </summary>
        /// <returns>Total number of linked nodes in bdd.</returns>
        public int CountNodes()
        {
            var roundedNodes = new List<Node>();
            foreach (var root in Roots)
            {
                DoRoundNodes(root, roundedNodes);
            }

            return roundedNodes.Count;
        }

        /// <summary>
        /// Performs bdd rounding and memorizes all rounded nodes.
        /// </summary>
        /// <param name="currentNode">Currently rounded node.</param>
        /// <param name="roundedNodes">A list of all rounded nodex.</param>
        /// <returns></returns>
        private static void DoRoundNodes(Node currentNode, List<Node> roundedNodes = null)
        {
            if (ReferenceEquals(roundedNodes, null))
            {
                roundedNodes = new List<Node>();
            }

            if (roundedNodes.Contains(currentNode))
            {
                // this node has already been rounded
                return;
            }

            roundedNodes.Add(currentNode);

            // rounding children
            var children = currentNode.Children.Select(edge => edge.Child).ToList();
            foreach (var child in children)
            {
                DoRoundNodes(child, roundedNodes);
            }

            return;
        }

        /// <summary>
        /// Performs simplification operation on bdd to build more compact equivalent bdd.
        /// </summary>
        public virtual void Optimize()
        {
            // implement in child classes
            return;
        }

        /// <summary>
        /// Validates whether roots are specified.
        /// </summary>
        /// <returns>True if bdd has roots.</returns>
        public bool ValidateRoots()
        {
            return Roots.Count > 0;
        }


        /// <summary>
        /// Validates whether sinks are specified.
        /// </summary>
        /// <returns>True if bdd has sinks.</returns>
        public bool ValidateSinks()
        {
            return Sinks.Count > 0;
        }

        /// <summary>
        /// Validates whether all non-terminal roots has two outgoing edges of types True and False.
        /// </summary>
        /// <returns>True if all edges constructed properly.</returns>
        public bool ValidateEdges()
        {
            return !Roots.Any(root => !DoValidateEdges(root));
        }

        /// <summary>
        /// Validates all edges by rounding bdd.
        /// </summary>
        /// <param name="currentNode">Currently rounding bdd.</param>
        /// <returns>True if edges of current node are valid.</returns>
        private static bool DoValidateEdges(Node currentNode)
        {
            if (currentNode.Children.Count == 0)
            {
                // terminal node
                return true;
            }

            if (currentNode.Children.Count != 2 ||
                currentNode.Children[0].Type == currentNode.Children[1].Type)
            {
                // invalid edges, in bdd each non-terminal node must have two edges of types True and False.
                return false;
            }

            // validating children
            var children = currentNode.Children.Select(edge => edge.Child);
            return !children.Any(child => !DoValidateEdges(child));
        }

        /// <summary>
        /// Validates whether all linked roots specified in bdd.
        /// </summary>
        /// <returns>True if all found roots are specified in bdd Roots property.</returns>
        public bool ValideteRootsCompleteness()
        {
            return !Sinks.Any(sink => !DoValidateRootsCompleteness(sink));
        }

        /// <summary>
        /// Searches for all roots linked from sinks by chain of internal nodes and checkes whether all found roots are specified in Roots property of bdd.
        /// </summary>
        /// <param name="currentNode">Currently rounded node.</param>
        /// <returns>True if parents of current node are internal nodes or root nodes specified in Roots property of bdd.</returns>
        private bool DoValidateRootsCompleteness(Node currentNode)
        {
            var parents = currentNode.Parents.Select(edge => edge.Parent);
            if (parents.Any(parent => parent.Parents.Count == 0 && !Roots.Contains(parent)))
            {
                return false;
            }

            // going up
            return !parents.Any(parent => !DoValidateRootsCompleteness(parent));
        }

        /// <summary>
        /// Validates whether all linked sinks specified in bdd.
        /// </summary>
        /// <returns>True if all found sinks are specified in bdd Sinks property.</returns>
        public bool ValideteSinksCompleteness()
        {
            return !Roots.Any(root => !DoValidateSinksCompleteness(root));
        }

        /// <summary>
        /// Searches for all sinks linked from roots by chain of internal nodes and checkes whether all found sinks are specified in Sinks property of bdd.
        /// </summary>
        /// <param name="currentNode">Currently rounded node.</param>
        /// <returns>True if children of current node are internal nodes or sink nodes specified in Sinks property of bdd.</returns>
        private bool DoValidateSinksCompleteness(Node currentNode)
        {
            var children = currentNode.Children.Select(edge => edge.Child);
            if (children.Any(child => child.Children.Count == 0 && !Sinks.Contains(child)))
            {
                return false;
            }

            // going down
            return !children.Any(child => !DoValidateSinksCompleteness(child));
        }

        /// <summary>
        /// Validate structure of bdd. It's a compute-intensive operation.
        /// </summary>
        /// <returns>True if bdd structure is ok.</returns>
        public virtual bool ValidateStructure()
        {
            // validating roots
            if (!ValidateRoots())
            {
                return false;
            }

            // validating sinks
            if (!ValidateSinks())
            {
                return false;
            }

            // validating edges
            if (!ValidateEdges())
            {
                return false;
            }

            // checking whether all roots are specified in Roots property
            if (!ValideteRootsCompleteness())
            {
                return false;
            }

            // checking whether all sinks are specified in Sinks property
            if (!ValideteSinksCompleteness())
            {
                return false;
            }

            return true;
        }
    }

    /// <summary>
    /// Element of a path in bdd.
    /// </summary>
    class PathElement
    {
        public Node Node;
        public BooleanValue Sign;
    }
}
